k:Knd, T, B:Type, l:IdLnk, ds:x:Id fp Type, tg:Id, f:(State(ds)TB), es:ES.
usends1-p(es;ds;k;T;l;tg;B;f)
 (g:{e:E| loc(e) = source(l)  Id & kind(e) = k} E
 ((e:{e:E| loc(e) = source(l)  Id & kind(e) = k} .
 ((kind(g(e)) = rcv(l,tg)  Knd)
 (c (sender(g(e)) = e
 (c & (e'':E. (kind(e'') = rcv(l,tg)  Knd)  (sender(e'') = e)  (e'' = g(e)))
 (c & val(g(e)) = f((state when e),val(e))))) 

latex

Definitions	t.1, True, T, , A c B, x:A. B(x), P & Q, x. t(x), t  T, P  Q, x:A. B(x), {T}, x(s), e@i. P(e), usends1-p(es;ds;k;T;l;tg;B;f)
Lemmas	es-loc-rcv, ldst wf, true wf, squash wf, es-vartype wf, es-state-subtype, es-state-when wf, es-val wf, es-kind-rcv, es-sender wf, es-kind wf, lsrc wf, es-loc wf, es-E wf, Knd wf, IdLnk wf, fpf wf, Id wf, decl-state wf, event system wf, usends1-p wf